Nuprl Lemma : pairwise-singleton
0,22
postcript
pdf
P
,
v
:Top. (
x
,
y
[
v
].
P
(
x
,
y
))
True
latex
Definitions
Top
,
(
x
,
y
L
.
P
(
x
;
y
))
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
x
(
s1
,
s2
)
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
True
Lemmas
true
wf
,
int
seg
wf
,
top
wf
origin
P, v:Top. (x,y
[v].P(x,y)) 
True P, v:Top. (x,y[v].P(x,y)) True x,yL.P(x;y)) Q
Q Q
}x:A. B(x) T